(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 117)) (_ BitVec 126))
(declare-fun p0 ( (_ BitVec 44) (_ BitVec 42) (_ BitVec 64)) Bool)
(declare-fun v0 () (_ BitVec 105))
(declare-fun v1 () (_ BitVec 94))
(declare-fun v2 () (_ BitVec 56))
(declare-fun v3 () (_ BitVec 55))
(declare-fun v4 () (_ BitVec 93))
(assert (let ((e5(_ bv163293995013 41)))
(let ((e6 (f0 ((_ sign_extend 61) v2))))
(let ((e7 (ite (p0 ((_ extract 66 23) v0) ((_ extract 42 1) v2) ((_ sign_extend 8) v2)) (_ bv1 1) (_ bv0 1))))
(let ((e8 (bvand ((_ zero_extend 125) e7) e6)))
(let ((e9 (bvcomp v1 ((_ sign_extend 39) v3))))
(let ((e10 (ite (= (_ bv1 1) ((_ extract 33 33) v3)) e5 ((_ zero_extend 40) e7))))
(let ((e11 ((_ rotate_left 0) e7)))
(let ((e12 (bvneg e8)))
(let ((e13 (bvnand ((_ zero_extend 49) v2) v0)))
(let ((e14 (bvcomp e5 ((_ zero_extend 40) e7))))
(let ((e15 (ite (bvule ((_ sign_extend 53) e10) v1) (_ bv1 1) (_ bv0 1))))
(let ((e16 (bvnor ((_ zero_extend 21) e13) e6)))
(let ((e17 (ite (bvult e16 ((_ zero_extend 125) e15)) (_ bv1 1) (_ bv0 1))))
(let ((e18 (ite (bvugt v1 ((_ sign_extend 93) e15)) (_ bv1 1) (_ bv0 1))))
(let ((e19 (bvsub v0 e13)))
(let ((e20 ((_ zero_extend 85) e15)))
(let ((e21 (bvsdiv ((_ sign_extend 125) e7) e8)))
(let ((e22 (bvneg e8)))
(let ((e23 (bvxor e19 ((_ sign_extend 104) e11))))
(let ((e24 ((_ rotate_right 10) e20)))
(let ((e25 (ite (bvult ((_ zero_extend 21) e19) e6) (_ bv1 1) (_ bv0 1))))
(let ((e26 (bvadd ((_ sign_extend 125) e7) e12)))
(let ((e27 (bvadd e13 ((_ sign_extend 104) e7))))
(let ((e28 ((_ extract 0 0) e15)))
(let ((e29 (ite (bvugt e22 ((_ zero_extend 125) e9)) (_ bv1 1) (_ bv0 1))))
(let ((e30 (ite (bvsle e10 e10) (_ bv1 1) (_ bv0 1))))
(let ((e31 (bvurem ((_ zero_extend 125) e30) e16)))
(let ((e32 (bvxnor e22 e31)))
(let ((e33 (bvurem e6 e16)))
(let ((e34 (bvneg v0)))
(let ((e35 (bvurem ((_ sign_extend 125) e15) e31)))
(let ((e36 (bvmul ((_ zero_extend 71) v3) e26)))
(let ((e37 (bvsrem ((_ zero_extend 104) e25) e19)))
(let ((e38 (bvxor v2 ((_ sign_extend 55) e25))))
(let ((e39 (ite (p0 ((_ zero_extend 43) e17) ((_ extract 61 20) e34) ((_ extract 65 2) e24)) (_ bv1 1) (_ bv0 1))))
(let ((e40 (ite (= (_ bv1 1) ((_ extract 89 89) e6)) ((_ sign_extend 104) e29) e23)))
(let ((e41 (bvnot e39)))
(let ((e42 (bvsdiv e19 e34)))
(let ((e43 (bvor e8 e12)))
(let ((e44 (ite (bvule e42 ((_ zero_extend 104) e14)) (_ bv1 1) (_ bv0 1))))
(let ((e45 (bvneg e14)))
(let ((e46 (concat e38 e29)))
(let ((e47 (ite (distinct e40 ((_ zero_extend 104) e18)) (_ bv1 1) (_ bv0 1))))
(let ((e48 (ite (bvsle e38 ((_ sign_extend 55) e29)) (_ bv1 1) (_ bv0 1))))
(let ((e49 (ite (bvult e40 ((_ zero_extend 64) e10)) (_ bv1 1) (_ bv0 1))))
(let ((e50 (ite (= e22 ((_ sign_extend 33) v4)) (_ bv1 1) (_ bv0 1))))
(let ((e51 (bvsle e12 e12)))
(let ((e52 (p0 ((_ extract 119 76) e12) ((_ extract 67 26) e27) ((_ zero_extend 63) e29))))
(let ((e53 (p0 ((_ extract 86 43) v1) ((_ zero_extend 41) e28) ((_ sign_extend 23) e10))))
(let ((e54 (bvult e22 ((_ zero_extend 125) e44))))
(let ((e55 (bvsgt ((_ sign_extend 31) v3) e20)))
(let ((e56 (bvuge e13 e19)))
(let ((e57 (bvsgt ((_ sign_extend 85) e25) e24)))
(let ((e58 (bvult v1 ((_ sign_extend 93) e18))))
(let ((e59 (= ((_ zero_extend 64) e10) e34)))
(let ((e60 (= e40 e37)))
(let ((e61 (bvugt v2 ((_ zero_extend 55) e49))))
(let ((e62 (distinct e23 ((_ zero_extend 104) e29))))
(let ((e63 (bvule e32 ((_ sign_extend 125) e45))))
(let ((e64 (bvslt ((_ zero_extend 2) v3) e46)))
(let ((e65 (= ((_ sign_extend 40) e14) e5)))
(let ((e66 (bvuge e31 ((_ zero_extend 21) e34))))
(let ((e67 (distinct ((_ sign_extend 85) e17) e20)))
(let ((e68 (bvsge e22 ((_ sign_extend 85) e5))))
(let ((e69 (= v3 ((_ zero_extend 54) e7))))
(let ((e70 (bvult e24 ((_ zero_extend 85) e49))))
(let ((e71 (p0 ((_ extract 100 57) e42) ((_ sign_extend 41) e18) ((_ extract 81 18) e26))))
(let ((e72 (bvult e36 e43)))
(let ((e73 (bvule e26 e43)))
(let ((e74 (bvslt e40 ((_ zero_extend 104) e47))))
(let ((e75 (bvugt e35 e43)))
(let ((e76 (bvsgt e28 e50)))
(let ((e77 (bvsgt ((_ zero_extend 55) e29) v2)))
(let ((e78 (= e27 e27)))
(let ((e79 (distinct e36 ((_ sign_extend 21) e37))))
(let ((e80 (bvule ((_ zero_extend 104) e50) e42)))
(let ((e81 (distinct ((_ sign_extend 32) v1) e8)))
(let ((e82 (bvult e6 ((_ zero_extend 21) e27))))
(let ((e83 (p0 ((_ sign_extend 43) e44) ((_ extract 86 45) e8) ((_ extract 78 15) e19))))
(let ((e84 (bvugt e43 ((_ sign_extend 125) e48))))
(let ((e85 (bvsle ((_ zero_extend 40) e50) e5)))
(let ((e86 (bvslt ((_ sign_extend 125) e48) e21)))
(let ((e87 (distinct e36 e8)))
(let ((e88 (bvuge ((_ sign_extend 70) e38) e12)))
(let ((e89 (distinct e42 e19)))
(let ((e90 (= ((_ sign_extend 125) e45) e22)))
(let ((e91 (bvsle e23 ((_ sign_extend 104) e45))))
(let ((e92 (bvsle e16 ((_ zero_extend 125) e30))))
(let ((e93 (bvsgt ((_ zero_extend 104) e9) e27)))
(let ((e94 (p0 ((_ sign_extend 43) e47) ((_ extract 41 0) v3) ((_ sign_extend 63) e50))))
(let ((e95 (p0 ((_ extract 121 78) e21) ((_ extract 83 42) e35) ((_ sign_extend 63) e18))))
(let ((e96 (bvsgt ((_ zero_extend 70) v2) e6)))
(let ((e97 (= e42 ((_ zero_extend 104) e48))))
(let ((e98 (= v2 ((_ zero_extend 15) e5))))
(let ((e99 (bvsgt e21 ((_ zero_extend 125) e41))))
(let ((e100 (bvslt ((_ sign_extend 71) v3) e31)))
(let ((e101 (p0 ((_ sign_extend 43) e14) ((_ zero_extend 41) e49) ((_ extract 74 11) e33))))
(let ((e102 (distinct e21 e8)))
(let ((e103 (bvsge e9 e9)))
(let ((e104 (bvuge ((_ zero_extend 125) e7) e12)))
(let ((e105 (bvugt ((_ zero_extend 93) e41) v1)))
(let ((e106 (bvult ((_ zero_extend 33) v4) e8)))
(let ((e107 (bvslt e36 ((_ sign_extend 125) e17))))
(let ((e108 (bvuge ((_ sign_extend 21) e40) e32)))
(let ((e109 (bvsle e43 ((_ zero_extend 33) v4))))
(let ((e110 (= ((_ zero_extend 21) e34) e33)))
(let ((e111 (bvule ((_ sign_extend 71) v3) e22)))
(let ((e112 (p0 ((_ extract 78 35) v0) ((_ sign_extend 41) e25) ((_ zero_extend 63) e9))))
(let ((e113 (bvugt e48 e14)))
(let ((e114 (bvslt e21 e6)))
(let ((e115 (bvugt e35 ((_ zero_extend 21) e42))))
(let ((e116 (bvsgt e8 ((_ sign_extend 33) v4))))
(let ((e117 (bvsge e48 e18)))
(let ((e118 (bvuge e26 e21)))
(let ((e119 (= e21 ((_ zero_extend 40) e20))))
(let ((e120 (bvugt e27 e19)))
(let ((e121 (p0 ((_ zero_extend 43) e39) ((_ sign_extend 41) e25) ((_ sign_extend 63) e30))))
(let ((e122 (bvslt e19 e40)))
(let ((e123 (p0 ((_ extract 63 20) e42) ((_ extract 121 80) e21) ((_ extract 89 26) e42))))
(let ((e124 (bvsge v0 ((_ sign_extend 104) e45))))
(let ((e125 (bvugt e50 e45)))
(let ((e126 (bvslt e21 ((_ zero_extend 33) v4))))
(let ((e127 (bvuge e23 ((_ zero_extend 104) e30))))
(let ((e128 (= e26 ((_ sign_extend 125) e7))))
(let ((e129 (bvsge ((_ sign_extend 71) v3) e33)))
(let ((e130 (= v3 ((_ sign_extend 54) e48))))
(let ((e131 (bvugt e25 e39)))
(let ((e132 (bvsgt ((_ sign_extend 104) e45) e23)))
(let ((e133 (bvuge e36 e12)))
(let ((e134 (bvslt e6 e33)))
(let ((e135 (= ((_ sign_extend 125) e39) e8)))
(let ((e136 (bvult ((_ sign_extend 85) e9) e20)))
(let ((e137 (= e38 ((_ zero_extend 55) e48))))
(let ((e138 (bvult e23 ((_ zero_extend 104) e48))))
(let ((e139 (bvuge e43 ((_ sign_extend 70) e38))))
(let ((e140 (= e31 ((_ zero_extend 70) e38))))
(let ((e141 (bvuge e47 e29)))
(let ((e142 (bvslt e23 ((_ zero_extend 50) v3))))
(let ((e143 (= e10 ((_ zero_extend 40) e39))))
(let ((e144 (bvsgt e13 e34)))
(let ((e145 (distinct e8 ((_ sign_extend 21) e37))))
(let ((e146 (bvule ((_ sign_extend 125) e48) e32)))
(let ((e147 (bvslt ((_ zero_extend 21) v0) e35)))
(let ((e148 (distinct e49 e9)))
(let ((e149 (bvsgt v0 ((_ sign_extend 11) v1))))
(let ((e150 (bvult ((_ sign_extend 125) e30) e12)))
(let ((e151 (bvsle v3 ((_ zero_extend 54) e30))))
(let ((e152 (bvugt e21 ((_ zero_extend 125) e47))))
(let ((e153 (bvuge e27 e42)))
(let ((e154 (= ((_ zero_extend 104) e39) e42)))
(let ((e155 (bvslt e42 ((_ zero_extend 104) e14))))
(let ((e156 (bvult e35 e36)))
(let ((e157 (bvsge ((_ zero_extend 21) e13) e21)))
(let ((e158 (distinct e50 e25)))
(let ((e159 (bvugt v1 ((_ zero_extend 93) e11))))
(let ((e160 (bvule ((_ zero_extend 104) e45) e34)))
(let ((e161 (bvsge e12 ((_ zero_extend 125) e9))))
(let ((e162 (bvugt ((_ zero_extend 40) e7) e5)))
(let ((e163 (bvsgt e33 ((_ sign_extend 21) e27))))
(let ((e164 (bvsle e41 e25)))
(let ((e165 (bvsgt e26 ((_ zero_extend 125) e7))))
(let ((e166 (bvslt ((_ sign_extend 104) e47) e42)))
(let ((e167 (bvslt e20 ((_ sign_extend 85) e45))))
(let ((e168 (bvsge e44 e47)))
(let ((e169 (bvsge v2 ((_ zero_extend 55) e29))))
(let ((e170 (bvslt v2 ((_ zero_extend 55) e30))))
(let ((e171 (bvugt e46 ((_ zero_extend 56) e9))))
(let ((e172 (bvsgt e45 e11)))
(let ((e173 (bvuge ((_ zero_extend 21) e34) e8)))
(let ((e174 (bvule e29 e39)))
(let ((e175 (= ((_ zero_extend 104) e15) v0)))
(let ((e176 (and e137 e162)))
(let ((e177 (not e69)))
(let ((e178 (=> e153 e58)))
(let ((e179 (and e117 e80)))
(let ((e180 (and e101 e92)))
(let ((e181 (not e79)))
(let ((e182 (ite e91 e126 e168)))
(let ((e183 (=> e55 e59)))
(let ((e184 (ite e56 e122 e100)))
(let ((e185 (or e53 e96)))
(let ((e186 (not e63)))
(let ((e187 (and e75 e174)))
(let ((e188 (xor e105 e86)))
(let ((e189 (ite e171 e169 e184)))
(let ((e190 (xor e134 e181)))
(let ((e191 (ite e139 e88 e103)))
(let ((e192 (and e52 e120)))
(let ((e193 (or e185 e62)))
(let ((e194 (or e149 e68)))
(let ((e195 (not e167)))
(let ((e196 (or e150 e98)))
(let ((e197 (=> e177 e102)))
(let ((e198 (=> e165 e65)))
(let ((e199 (or e187 e198)))
(let ((e200 (ite e119 e76 e76)))
(let ((e201 (not e159)))
(let ((e202 (ite e121 e112 e148)))
(let ((e203 (xor e192 e61)))
(let ((e204 (not e81)))
(let ((e205 (not e128)))
(let ((e206 (or e130 e170)))
(let ((e207 (xor e77 e186)))
(let ((e208 (ite e82 e115 e127)))
(let ((e209 (= e189 e133)))
(let ((e210 (and e183 e188)))
(let ((e211 (= e64 e200)))
(let ((e212 (xor e90 e118)))
(let ((e213 (= e201 e147)))
(let ((e214 (or e152 e140)))
(let ((e215 (ite e190 e145 e138)))
(let ((e216 (= e199 e116)))
(let ((e217 (or e73 e73)))
(let ((e218 (ite e158 e204 e84)))
(let ((e219 (xor e83 e83)))
(let ((e220 (xor e208 e214)))
(let ((e221 (= e146 e218)))
(let ((e222 (or e132 e206)))
(let ((e223 (and e205 e67)))
(let ((e224 (ite e217 e104 e212)))
(let ((e225 (=> e99 e211)))
(let ((e226 (ite e176 e151 e210)))
(let ((e227 (or e207 e70)))
(let ((e228 (ite e219 e164 e72)))
(let ((e229 (and e144 e203)))
(let ((e230 (ite e222 e216 e93)))
(let ((e231 (xor e166 e182)))
(let ((e232 (and e157 e143)))
(let ((e233 (=> e129 e60)))
(let ((e234 (=> e225 e179)))
(let ((e235 (ite e95 e135 e213)))
(let ((e236 (or e161 e173)))
(let ((e237 (= e78 e172)))
(let ((e238 (or e231 e108)))
(let ((e239 (=> e154 e109)))
(let ((e240 (and e193 e175)))
(let ((e241 (not e125)))
(let ((e242 (not e221)))
(let ((e243 (xor e94 e111)))
(let ((e244 (ite e197 e237 e110)))
(let ((e245 (or e107 e156)))
(let ((e246 (and e209 e131)))
(let ((e247 (not e141)))
(let ((e248 (= e227 e244)))
(let ((e249 (xor e51 e243)))
(let ((e250 (and e155 e113)))
(let ((e251 (or e250 e234)))
(let ((e252 (xor e249 e232)))
(let ((e253 (= e241 e136)))
(let ((e254 (= e252 e242)))
(let ((e255 (xor e220 e224)))
(let ((e256 (ite e163 e254 e57)))
(let ((e257 (=> e195 e180)))
(let ((e258 (= e239 e202)))
(let ((e259 (or e87 e123)))
(let ((e260 (=> e229 e54)))
(let ((e261 (ite e196 e196 e142)))
(let ((e262 (ite e106 e245 e255)))
(let ((e263 (xor e238 e257)))
(let ((e264 (=> e259 e246)))
(let ((e265 (ite e264 e253 e194)))
(let ((e266 (=> e248 e256)))
(let ((e267 (not e215)))
(let ((e268 (xor e236 e89)))
(let ((e269 (ite e71 e266 e71)))
(let ((e270 (not e230)))
(let ((e271 (xor e268 e235)))
(let ((e272 (=> e263 e262)))
(let ((e273 (= e178 e258)))
(let ((e274 (=> e191 e269)))
(let ((e275 (or e66 e260)))
(let ((e276 (and e85 e233)))
(let ((e277 (xor e251 e267)))
(let ((e278 (xor e265 e160)))
(let ((e279 (ite e275 e247 e275)))
(let ((e280 (not e273)))
(let ((e281 (ite e278 e228 e124)))
(let ((e282 (or e270 e271)))
(let ((e283 (or e276 e74)))
(let ((e284 (and e283 e223)))
(let ((e285 (and e261 e240)))
(let ((e286 (and e97 e282)))
(let ((e287 (= e279 e280)))
(let ((e288 (and e272 e285)))
(let ((e289 (not e288)))
(let ((e290 (= e281 e114)))
(let ((e291 (= e287 e226)))
(let ((e292 (and e284 e290)))
(let ((e293 (not e291)))
(let ((e294 (=> e274 e277)))
(let ((e295 (xor e293 e289)))
(let ((e296 (= e295 e295)))
(let ((e297 (not e294)))
(let ((e298 (or e296 e296)))
(let ((e299 (not e292)))
(let ((e300 (or e297 e299)))
(let ((e301 (and e300 e300)))
(let ((e302 (= e298 e301)))
(let ((e303 (or e302 e286)))
(let ((e304 (and e303 (not (= e34 (_ bv0 105))))))
(let ((e305 (and e304 (not (= e34 (bvnot (_ bv0 105)))))))
(let ((e306 (and e305 (not (= e31 (_ bv0 126))))))
(let ((e307 (and e306 (not (= e19 (_ bv0 105))))))
(let ((e308 (and e307 (not (= e19 (bvnot (_ bv0 105)))))))
(let ((e309 (and e308 (not (= e8 (_ bv0 126))))))
(let ((e310 (and e309 (not (= e8 (bvnot (_ bv0 126)))))))
(let ((e311 (and e310 (not (= e16 (_ bv0 126))))))
e311
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
